% TEMPORAL REASONING
% thom fruehwirth ECRC 920721
% follows work by Itay Meiri AAAI 1991
% uses path concistency handler pc.chr
% 930908 updated and modified for new CHR version

handler time.


:- ['time-pc.pl']. 	% get compiled path consistency handler


%% domain specific predicates ------------------------------------------------

%alldiff(L) :- \+ (append(_,[X|L1],L),member(Y,L1),X==Y). % quick hack

ground(X):- not nonground(X).

	inf(3.40282e38).
	minf((-3.40282e38)).
	sup(1e-45).
	msup((-1e-45)).


delay empty(N,L,T) if var(N),var(L).
empty(0,[],T).

delay universal(N,L,T) if var(N).
delay universal(N,L,T) if var(L).
delay universal(N,L,T) if var(T).
universal(N,L,T):-
	(is_quantl(L) -> 
		L=[A-B],(A=<minf),(inf=<B)
		; 
	T=p-p -> 		% 930212 to account for finite domains
		sort(L,[eq, ge, le])
		;
		size(T,N)
	),
	!.

	size(i-i,13).
	size(p-p,3).
	size(p-i,5).
	size(i-p,5).
	size(s-s,5).

delay equality(L,T) if var(T).
delay equality(L,T) if var(L).
equality(L,i-i):- !, member(equals,L).
equality(L,s-s):- !, member(eq,L).
equality(L,p-p):-
	(is_quall(L) ->			% succeeds also if var-case: dirty!!
		member(E,L),(E=eq;number(E),E=:=0)	% 930212
		;
		member(A-B,L),
		(A=0,B=0 ; (A=<0),(0=<B))
	),
	!.

delay unique(L) if nonground(L).
unique([A-B]):- !,(A=:=B).
unique([A]).

% 930212 for finite domains
bind_value(X,Y,[R]):- (R=V-_;R=V)->(Y=:=X+V).

shift_interval(X,[],[]).
shift_interval(X,[A-C|L1],[B-D|L2]):- !,
	B is A-X, D is C-X,
	shift_interval(X,L1,L2).
shift_interval(X,[A|L1],[B|L2]):-
	B is A-X,
	shift_interval(X,L1,L2).


delay intersection(L1,L2,L3,T) if var(L1).
delay intersection(L1,L2,L3,T) if var(L2).
intersection(L1,L2,L3,T):- qtype(L1,Q1),qtype(L2,Q2),
		((Q1==quall,Q2==quall) ->
			intersection(L1,L2,L3)	% built-in
			;
			qualquant(L1,Q1,LQ1),qualquant(L2,Q2,LQ2),
			interint(LQ1,LQ2,L3)
		),
		!. 

  % interint([1-2,4-5,6-9],[2-3,3-11],L).
  interint([],L,[]).
  interint(L,[],[]):- L=[_|_].
  interint([A|L1],[B|L2],L3):-
	(
	 isless(A,B) -> interint(L1,[B|L2],L3);
	 isless(B,A) -> interint([A|L1],L2,L3);
	 overlaps1(A,B,C) -> L3=[C|L3N],interint([A|L1],L2,L3N);
	 overlaps2(A,B,C) -> L3=[C|L3N],interint(L1,[B|L2],L3N)
	).

    isless(A-B,C-D):- (B<C).

    overlaps1(A-B,C-D,E-F):- 
	(B>=D),(C=<B),(A=<D), 
	my_max(A,C,E),my_min(B,D,F).
%	E is max(float(A),float(C)), F is min(float(B),float(D)).
    overlaps2(A-B,C-D,E-F):- 
	(D>=B),(C=<B),(A=<D), 
	my_max(A,C,E),my_min(B,D,F).
%	E is max(float(A),float(C)), F is min(float(B),float(D)).

	my_max(X,Y,Z):- (X>=Y),!,X=Z.
	my_max(X,Y,Y).

	my_min(X,Y,Z):- (X=<Y),!,X=Z.
	my_min(X,Y,Y).

delay transl(A,B,C,T) if var(A),var(B).
delay transl(A,B,C,T) if var(A),var(C).
delay transl(A,B,C,T) if var(B),var(C).
transl(A,B,C,T):- 
	qtype(A,QA),qtype(B,QB),qtype(C,QC),	
	(
	(T=p-p-p,(QA==quantl;QB==quantl;QC==quantl) ) ->  % at least one quantl
		qualquant(A,QA,A1),qualquant(B,QB,B1),qualquant(C,QC,C1),
		transl(A1,B1,C1,T,quantl)
		;
		quantqual(A,QA,A1),quantqual(B,QB,B1),quantqual(C,QC,C1),
		transl(A1,B1,C1,T,quall)
	),
	!.	

  transl(L1,L2,L3,T,Q):- var(L3),!,
	setof(C,A^B^(member(A,L1),member(B,L2),trans(A,B,C,T,Q)),L3N),
	mergerel(L3N,L3,T,Q).
  transl(L1,L2,L3,T,Q):- var(L2),!,
	setof(B,A^C^(member(A,L1),member(C,L3),trans(A,B,C,T,Q)),L2N),
	mergerel(L2N,L2,T,Q).
  transl(L1,L2,L3,T,Q):- var(L1),!,
	setof(A,B^C^(member(B,L2),member(C,L3),trans(A,B,C,T,Q)),L1N),
	mergerel(L1N,L1,T,Q).

	mergerel(L1,L2,T,Q):- 
		(Q==quantl -> mergerel(L1,L2) ; L1=L2),
		!.
	  mergerel([],[]).
	  mergerel([A-B,C-D|L1],L2):-
		(B+sup>=C),		% +sup added 921029
		!,
		my_min(A,C,Min),		% min, max added 920129
		my_max(B,D,Max),
		mergerel([Min-Max|L1],L2).
	  mergerel([X|L1],[X|L2]):-
		mergerel(L1,L2).

     trans(A,B,C,s-s-s,quall):- !, 
		strans(A,B,C).
     trans(A,B,C,p-p-p,quall):- !, 
		prans(A,B,C).
     trans(A,B,C,p-p-p,quantl):- !, 
		qtrans(A,B,C).
     trans(A,B,C,U-V-W,quall):- !,
		itrans(U-V-W,A,B,C). 


%% qualitative and quantitative constraints interaction

delay qtype(L,Q) if nonground(L).
qtype(L,quantl):- is_quantl(L).
qtype(L,quall):- is_quall(L).

 is_quantl([X|_]):- is_quant(X).
 is_quall([X|_]):- is_qual(X).

  delay is_quant(A) if var(A).
  is_quant(A-B). % :- A1 is A,B1 is B,number(A1),number(B1).
  delay is_qual(A) if var(A).
  is_qual(A):- atomic(A).	% single numbers are treated like atoms 930212

   delay qualquant(A,QA,A1) if var(A),var(A1).	% necessary?
   qualquant(A,QA,A1):- 	% hacked for var-case (== versus = below!)
		(QA==quall -> qualquant(A,A0),mergerel(A0,A1) ; QA=quantl -> A=A1).	% mergrel added 921029

   delay quantqual(A,QA,A1) if var(A),var(A1).	% necessary?
   quantqual(A,QA,A1):- 	% hacked for var-case (== versus = below!)
		(QA==quantl -> quantqual(A,A1) ; QA=quall -> A=A1).

%path(N,X,Y,L,p-p) +=> qualquant(L,LIN), sort(LIN,LI), path(N,X,Y,LI,p-p).

	qualquant([],[]).
	qualquant([A|L1],[B|L2]):-
		qualquant1(A,B),
		qualquant(L1,L2).

		qualquant1(le,A-B):- !, A is sup, B is inf.
		qualquant1(eq,0-0):- !.
		qualquant1(ge,A-B):- !, A is minf, B is msup.
		% 930212 to treat single numbers 
		qualquant1(N,A-A):- A is N.	% 'is' used to catch type error

%path(N,X,Y,LI,p-p) +=> N>2 | 		% quick hack condition for termination
%	quantqual(LI,L), length(L,N1), path(N1,X,Y,L,p-p). 

	quantqual(LI,L):-
		findall(X,quantqual1(LI,X),L).

		quantqual1(LI,eq):- 
			once((member(I-J,LI), (I=<0),(0=<J))).
		quantqual1(LI,le):-  
			once((member(I-J,LI), (0<J))).
		quantqual1(LI,ge):-  
			once((member(I-J,LI), (I<0))).

		% 930212 to treat single numbers 
		quantqual1(LI,N):-  
			once((member(N-M,LI), (N=:=M))).




% ALLENS INTERVALS ---------------------------------------------------------

:- ['allentable.pl'].	% get cons_tri/3 transitivity table for Allens intervals

%[after, before, contains, during, equals, finished_by, finishes, meets, met_by, overlapped_by, overlaps, started_by, starts].

%930212
check_ii(X,Y,R):- interval_point(X,R,Y).	
% taken from jonathan lever
interval_point([X,Y],before,[U,V]):- ((Y < U)).
interval_point([X,Y],after,[U,V]):- ((V < X)).
interval_point([X,Y],meets,[U,V]):- ((Y =:= U)).
interval_point([X,Y],met_by,[U,V]):- ((V =:= X)).
interval_point([X,Y],starts,[U,V]):- ((X =:= U, Y < V)).
interval_point([X,Y],started_by,[U,V]):- ((X =:= U, V < Y)).
interval_point([X,Y],finishes,[U,V]):- ((Y =:= V, U < X)).
interval_point([X,Y],finished_by,[U,V]):- ((Y =:= V, X < V)).
interval_point([X,Y],during,[U,V]):- ((U < X, Y < V)).
interval_point([X,Y],contains,[U,V]):- ((X < U, V < Y)).
interval_point([X,Y],overlaps,[U,V]):- ((X < U, U < Y, Y < V)).
interval_point([X,Y],overlapped_by,[U,V]):- ((U < X, X < V, V < Y)).
interval_point([X,Y],equals,[U,V]):- ((X =:= U,Y =:= V)).


itrans(U-V-W,A,B,C):-	
		encode(U-V,A,X),encode(V-W,B,Y),encode(U-W,C,Z), 
		cons_tri(X,Y,Z).

delay encode(U-V,A,X) if var(A),var(X).
encode(i-i,A,B):-!,encode(A,B).
encode(p-i,A,B):-!,pi_ii(A,Y),encode(Y,B).
encode(i-p,A,B):-!,ip_ii(A,Y),encode(Y,B).
encode(p-p,A,B):-!,pp_pi(A,X),pi_ii(X,Y),encode(Y,B).

delay encode(A,X) if var(A),var(X).
encode(before,1).
encode(after,2).
encode(during,3).
encode(contains,4).
encode(overlaps,5).
encode(overlapped_by,6).
encode(meets,7).
encode(met_by,8).
encode(starts,9).
encode(started_by,10).
encode(finishes,11).
encode(finished_by,12).
encode(equals,13).



% POINT ALGEBRA ---------------------------------------------------------------

%[le,eq,ge]

% 930212
check_pp(X,Y,A-B):- !, ((X+A<Y,Y<X+B)).
check_pp(X,Y,N):- number(N),!, (X+N=:=Y).
check_pp(X,Y,T):- \+ member(T,[le,eq,ge]),!, Y=T.
check_pp(X,Y,R):- ((number(X),number(Y))->check_ppn(X,Y,R);check_ppt(X,Y,R)).

check_ppn(X,Y,le):- (X<Y).
check_ppn(X,Y,eq):- (X=:=Y).
check_ppn(X,Y,ge):- (X>Y).

check_ppt(X,Y,le):- (X@<Y).
check_ppt(X,Y,eq):- (X=Y).
check_ppt(X,Y,ge):- (X@>Y).

prans(A,B,C):- (number(A);number(B);number(C)),!,qtrans(A-A,B-B,C-C).
prans(le,le,le).
prans(le,eq,le).
prans(le,ge,le).
prans(le,ge,eq).
prans(le,ge,ge).
prans(eq,le,le).
prans(eq,eq,eq).
prans(eq,ge,ge).
prans(ge,le,le).
prans(ge,le,eq).
prans(ge,le,ge).
prans(ge,eq,ge).
prans(ge,ge,ge).

	




% QUANTITATIVE  ---------------------------------------------------------

% [I1-I2,...In-1-In] ordered Ii=<Ii+1, comparison problem with reals (equality)

qtrans(A-B,C-D,E-F):- (	(var(A),var(B)) -> safe_is(A,E-D), safe_is(B,F-C) ;
			(var(C),var(D)) -> safe_is(C,E-B), safe_is(D,F-A) ;
			(var(E),var(F)) -> safe_is(E,A+C), safe_is(F,B+D)
			).
	safe_is(A,X-Y):-
		((X=:=minf),(Y=:=inf)) -> A is minf
		;
		((X=:=inf),(Y=:=minf)) -> A is inf
		;
		((X=:=msup),(Y=:=sup)) -> A is msup
		;
		((X=:=sup),(Y=:=msup)) -> A is sup
		;
		A is X-Y.
	safe_is(A,X+Y):-
		((X=:=inf),(Y=:=inf)) -> A is inf
		;
		((X=:=minf),(Y=:=minf)) -> A is minf
		;
		((X=:=sup),(Y=:=sup)) -> A is sup
		;
		((X=:=msup),(Y=:=msup)) -> A is msup
		;
		A is X+Y.





% POINT-INTERVAL ---------------------------------------------------------

% p-i [before,starts,during,finishes,after]
% i-p [after,started_by,contains,finished_by,before]

%930212
check_pi(X,[A,B],before):- ((X<A)).
check_pi(X,[A,B],starts):- ((X=:=A)).
check_pi(X,[A,B],during):- ((A<X,X<B)).
check_pi(X,[A,B],finishes):- ((X=:=B)).
check_pi(X,[A,B],after):- ((B<X)).

check_pi([A,_B],X,after):- ((X<A)).
check_pi([A,_B],X,started_by):- ((X=:=A)).
check_pi([A,B],X,contains):- ((A<X,X<B)).
check_pi([_A,B],X,finished_by):- ((X=:=B)).
check_pi([_A,B],X,before):- ((B<X)).

% trans see itrans for INTERVAL

% pi_ii
delay pi_ii(A,B) if var(A),var(B).
pi_ii(before, before).
pi_ii(before, meets).
pi_ii(before, finished_by).
pi_ii(before, contains).
pi_ii(before, overlaps).
pi_ii(starts, starts).
pi_ii(starts, equals).
pi_ii(starts, started_by).
pi_ii(during, during).
pi_ii(during, finishes).
pi_ii(during, overlaped_by).
pi_ii(finishes, met_by).
pi_ii(after, after).

% ip_ii (inversion of pi_ii)
delay ip_ii(A,B) if var(A),var(B).
ip_ii(before, before).
ip_ii(finished_by, meets).
ip_ii(contains, contains).
ip_ii(contains, overlaps).
ip_ii(contains, finished_by).
ip_ii(started_by, starts).
ip_ii(started_by, equals).
ip_ii(started_by, started_by).
ip_ii(after, during).
ip_ii(after, finishes).
ip_ii(after, overlaped_by).
ip_ii(after, met_by).
ip_ii(after, after).

% pp_pi
delay pp_pi(A,B) if var(A),var(B).
pp_pi(le, before).
pp_pi(eq, starts).
pp_pi(ge, during).
pp_pi(ge, finishes).
pp_pi(ge, after).

% pp_ii
delay pp_ii(A,B) if var(A),var(B).
pp_ii(A,B):- pp_pi(A,C),pi_ii(C,B).



% end of handler time.chr ----------------------------------------------------